Termination proof of /tmp/tmpqmZy0Z/PALINDROME

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
and: {1}
tt: empty set
isList: empty set
isNeList: empty set
isQid: empty set
isNePal: empty set
isPal: empty set
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

↳ CSR

  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, __¹} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, ISNELIST, ISLIST, ISQID, ISNEPAL, ISPAL, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)
ISLIST(V) → ISNELIST(V)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(V) → ISQID(V)
ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
ISNEPAL(V) → ISQID(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))
ISNEPAL(__(I, __(P, I))) → ISQID(I)
ISPAL(V) → ISNEPAL(V)

The collapsing dependency pairs are DP_c:

AND(tt, X) → X

The hidden terms of R are:

isList(V2)
isNeList(V2)
isPal(P)

Every hiding context is built from:none

Hence, the new unhiding pairs DP_u are :

AND(tt, X) → U(X)
U(isList(V2)) → ISLIST(V2)
U(isNeList(V2)) → ISNELIST(V2)
U(isPal(P)) → ISPAL(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 3 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, ISNELIST, U, ISLIST, ISPAL, ISNEPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
AND(tt, X) → U(X)
U(isList(V2)) → ISLIST(V2)
ISLIST(V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
U(isNeList(V2)) → ISNELIST(V2)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(AND(x₁, x₂)) = x₂
POL(ISLIST(x₁)) = 1 + 2·x₁
POL(ISNELIST(x₁)) = 1 + 2·x₁
POL(ISNEPAL(x₁)) = 0
POL(ISPAL(x₁)) = 0
POL(U(x₁)) = x₁
POL(__(x₁, x₂)) = 2 + 2·x₁ + x₂
POL(a) = 1
POL(and(x₁, x₂)) = 2·x₁ + x₂
POL(e) = 1
POL(i) = 2
POL(isList(x₁)) = 2 + 2·x₁
POL(isNeList(x₁)) = 2 + 2·x₁
POL(isNePal(x₁)) = 0
POL(isPal(x₁)) = 0
POL(isQid(x₁)) = 0
POL(nil) = 0
POL(o) = 2
POL(tt) = 0
POL(u) = 1

the following usable rules

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
and(tt, X) → X
isPal(V) → isNePal(V)
isPal(nil) → tt
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))

could all be oriented weakly.
Furthermore, the pairs

ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
U(isList(V2)) → ISLIST(V2)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
U(isNeList(V2)) → ISNELIST(V2)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)
ISLIST(V) → ISNELIST(V)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, U, ISNELIST, ISLIST, ISPAL, ISNEPAL} are not replacing on any position.

The TRS P consists of the following rules:

AND(tt, X) → U(X)
ISLIST(V) → ISNELIST(V)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSUsableRulesProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, ISPAL, U, ISNEPAL} are not replacing on any position.

The TRS P consists of the following rules:

U(isPal(P)) → ISPAL(P)
ISPAL(V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))
AND(tt, X) → U(X)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The following rules are not useable and can be deleted:

__(__(x0, x1), x2) → __(x0, __(x1, x2))
__(x0, nil) → x0
__(nil, x0) → x0
and(tt, x0) → x0
isList(x0) → isNeList(x0)
isList(nil) → tt
isList(__(x0, x1)) → and(isList(x0), isList(x1))
isNeList(x0) → isQid(x0)
isNeList(__(x0, x1)) → and(isList(x0), isNeList(x1))
isNeList(__(x0, x1)) → and(isNeList(x0), isList(x1))
isNePal(x0) → isQid(x0)
isNePal(__(x0, __(x1, x0))) → and(isQid(x0), isPal(x1))
isPal(x0) → isNePal(x0)
isPal(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSUsableRulesProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {AND} we have µ(f) = {1}.
The symbols in {isQid, isPal, ISPAL, U, ISNEPAL} are not replacing on any position.

The TRS P consists of the following rules:

U(isPal(P)) → ISPAL(P)
ISPAL(V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))
AND(tt, X) → U(X)

The TRS R consists of the following rules:

isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

Using the order
Recursive path order with status [2].
Quasi-Precedence:

[isPal₁, ISPAL₁, ISNEPAL₁, isQid₁, tt, e] > [U₁, AND₂]
__₂ > [U₁, AND₂]
a > [U₁, AND₂]
i > [U₁, AND₂]
o > [U₁, AND₂]
u > [U₁, AND₂]

Status:

i: multiset
a: multiset
__₂: multiset
e: multiset
o: multiset
isQid₁: [1]
isPal₁: [1]
tt: multiset
ISPAL₁: [1]
u: multiset
AND₂: [2,1]
U₁: [1]
ISNEPAL₁: [1]

the following usable rules

isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

U(isPal(P)) → ISPAL(P)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))
AND(tt, X) → U(X)

could be oriented strictly and thus removed.
The pairs

ISPAL(V) → ISNEPAL(V)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSUsableRulesProof

                      ↳ QCSDP

                        ↳ QCSDPReductionPairProof

                          ↳ QCSDP

                            ↳ QCSDependencyGraphProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {isQid, ISNEPAL, ISPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISPAL(V) → ISNEPAL(V)

The TRS R consists of the following rules:

isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, __¹} are replacing on all positions.
For all symbols f in {and} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal} are not replacing on any position.

The TRS P consists of the following rules:

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
__¹(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → X
isList(V) → isNeList(V)
isList(nil) → tt
isList(__(V1, V2)) → and(isList(V1), isList(V2))
isNeList(V) → isQid(V)
isNeList(__(V1, V2)) → and(isList(V1), isNeList(V2))
isNeList(__(V1, V2)) → and(isNeList(V1), isList(V2))
isNePal(V) → isQid(V)
isNePal(__(I, __(P, I))) → and(isQid(I), isPal(P))
isPal(V) → isNePal(V)
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.